Standard Mathematical Logic
Meghdad Ghari; Fatemeh Majlesi
Abstract
Justification Logic is a family of modal logics in which the proof or justification of a necessitated proposition can be explicitly expressed. These logics can be considered as epistemic logics in which the justification (reason or evidence) for knowledge or belief of a proposition can be expressed in ...
Read More
Justification Logic is a family of modal logics in which the proof or justification of a necessitated proposition can be explicitly expressed. These logics can be considered as epistemic logics in which the justification (reason or evidence) for knowledge or belief of a proposition can be expressed in the language. In this paper, we study an extension of justification logics with actions. In particular, we extend the language of Artemov's logic of proofs with actions. To this end, we use the regular actions of propositional dynamic logic without the iteration operator. By combining the axiom system of the logic of proofs with that of propositional dynamic logic, we present an axiomatic proof system for this combined logic. We also present a possible world semantics, based on Kripke-Fitting models, for this combined logic, and prove the completeness theorem by means of the canonical model construction. We further establish the internalization property for this logic.
Meghdad Ghari
Abstract
In this note, we study the effect of adding fixed points to justification logics. By making use of the fixed point operators (or diagonal operators) introduced by Smorynski in his Diagonalization Operator Logic, we introduce fixed point extensions of Fitting's quantified logic of proofs QLP. We then ...
Read More
In this note, we study the effect of adding fixed points to justification logics. By making use of the fixed point operators (or diagonal operators) introduced by Smorynski in his Diagonalization Operator Logic, we introduce fixed point extensions of Fitting's quantified logic of proofs QLP. We then formalize the Knower Paradox and various self-reference versions of the Surprise Test Paradox in these fixed point extensions of QLP. By interpreting a surprise statement as a statement for which there is no justification or evidence, we propose a solution to the self-reference version of the Surprise Test paradox. We show that one of the axioms of QLP (the Uniform Barcan Formula) could be the reason for producing contradiction in these paradoxes, and thus by rejecting this axiom we can avoid contradiction in the aforementioned paradoxes. By introducing Mkrtychev models for the fixed point extensions of QLP, we further show that these fixed point extensions (without the Uniform Barcan Formula) are consistent.
